D realizes es. P(es)
== D':Dsys. D  D'  (w:World, p:FairFifo. PossibleWorld(D';w)  P(ES(w))) 

latex

---

clarification:

d-realizes{i:l}
d-realizes(D; es.P(es))
== D':dsys{i:l}.
== d-sub{i:l}
== d-sub(D; D')
==  (w:world{i:l}, p:fair-fifo{i:l}(w). possible-world{i:l}(D'; w)  P(w-es{i:l}(w; p))) 

latex

Definitions	Dsys, D1  D2, World, x:A. B(x), FairFifo, P  Q, PossibleWorld(D;w), ES(the_w)
FDL editor aliases	d-realizes